/*
 * Bogor: An Extensible and Highly-Modular Model Checking Framework Copyright
 * (c) 2002-2004 Kansas State University This software is licensed using the
 * SAnToS Laboratory Open Academic License. You should have received a copy of
 * the License in the top directory of this software distribution package. If
 * not, then write to SAnToS Laboratory, 234 Nichols Hall, Manhattan, KS 66506,
 * USA. The SAnToS Laboratory homepage is located at
 * http://www.cis.ksu.edu/santos. The Bogor homepage is located at
 * http://bogor.projects.cis.ksu.edu.
 */
package edu.ksu.cis.projects.bogor.module;


import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Properties;
import java.util.Set;

import edu.ksu.cis.projects.bogor.IBogorConfiguration;
import edu.ksu.cis.projects.bogor.ast.Exp;
import edu.ksu.cis.projects.bogor.ast.Location;
import edu.ksu.cis.projects.bogor.ast.Node;
import edu.ksu.cis.projects.bogor.ast.Transformation;
import edu.ksu.cis.projects.bogor.module.ConfigurationMessages;
import edu.ksu.cis.projects.bogor.module.DefaultMessageStore;
import edu.ksu.cis.projects.bogor.module.IEnabledTransformationsContext;
import edu.ksu.cis.projects.bogor.module.IExpEvaluator;
import edu.ksu.cis.projects.bogor.module.IMessageStore;
import edu.ksu.cis.projects.bogor.module.IModule;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategist;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyContext;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyInfo;
import edu.ksu.cis.projects.bogor.module.ISearcher;
import edu.ksu.cis.projects.bogor.module.ITransformationFilter;
import edu.ksu.cis.projects.bogor.module.IValueFactory;
import edu.ksu.cis.projects.bogor.module.backtrack.ITransformationBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.config.Domain;
import edu.ksu.cis.projects.bogor.module.config.ISelfDescribingModule;
import edu.ksu.cis.projects.bogor.module.config.OptionScope;
import edu.ksu.cis.projects.bogor.module.state.IState;
import edu.ksu.cis.projects.bogor.module.throwable.BogorException;
import edu.ksu.cis.projects.bogor.module.throwable.IllFormedModelBogorException;
import edu.ksu.cis.projects.bogor.module.value.IIntValue;
import edu.ksu.cis.projects.bogor.module.value.IValue;
import edu.ksu.cis.projects.bogor.symboltable.FSMSymbolTable;
import edu.ksu.cis.projects.bogor.symboltable.SymbolTable;
import edu.ksu.cis.projects.bogor.util.FileMessage;
import edu.ksu.cis.projects.bogor.util.Pair;
import edu.ksu.cis.projects.bogor.util.Triple;
import edu.ksu.cis.projects.bogor.util.Util;
import edu.ksu.cis.projects.trove.custom.IntList;
import edu.ksu.cis.projects.trove.custom.IntObjectTable;
import edu.ksu.cis.projects.trove.custom.LongIntTable;

/**
 * @author <a href="mailto:robby@cis.ksu.edu">Robby </a>
 * @version CVS $Revision: 1.33 $ $Date: 2005/08/08 21:42:35 $
 */
public class DefaultSchedulingStrategist
    implements ISchedulingStrategist, ISelfDescribingModule
{
    private static final ITransformationFilter[] EMPTY_FILTER_SET = {};

    // ~ Instance variables
    // .....................................................

    // .....................................................
    protected String TRUE_WHEN_FAILED_ID = "trueWhenFailed";

    protected String FALSE_WHEN_FAILED_ID = "falseWhenFailed";

    protected String EXCEPTION_WHEN_FAILED_ID = "exceptionWhenFailed";

    /**
     * Configuration option
     */
    protected boolean trueWhenFailed = false;

    /**
     * Configuration option
     */
    protected boolean falseWhenFailed = false;

    /**
     * Configuration option
     */
    protected boolean exceptionWhenFailed = true;

    /**
     * Runtime module connection
     */
    protected SymbolTable symbolTable;

    /**
     * Runtime module connection
     */
    protected ISchedulingStrategist ss;

    /**
     * Runtime module connection      
     */
    protected IValueFactory vf;

    /**
     * Runtime module connection
     */
    protected IExpEvaluator ee;

    /**
     * Runtime module connection
     */
    protected ISearcher sr;

    /**
     * Tracks which nondeterministic branches have been taken inside a single
     * action node.
     */
    protected ISchedulingStrategyInfo currentSSI;

    /**
     * Points to the index of the current info record used inside
     * <code>currentSSI</code>.
     */
    protected int currentIndex;

    /**
     * Stateful variable
     */
    protected Node currentNode;

    /**
     * Stateful variable
     */
    protected NodeContext ec;

    /**
     * Stateful variable
     */
    protected HashMap<NodeContext, ISchedulingStrategyInfo> nodeSSIMap;

    /**
     * Stateful variable
     */
    protected LongIntTable transformationChooseMap;

    /**
     * Stateful variable
     */
    protected boolean interleavingSuppressed = false;

    /**
     * Java class names of the custom transformation filters.
     */
    protected String[] transformationFilterClassNames = new String[0];

    /**
     * Counter giving how many re-entrant levels of non-scripting we're in (used
     * to record whether a counterexample-trail scheduling info is generated).
     */
    protected int numNonScriptedScopes = 0;

    /**
     * An ordered series of filters which strip out transitions that are
     * otherwise enabled.
     */
    protected ITransformationFilter[] transformationFilters = EMPTY_FILTER_SET;

    // ~ Constructors
    // ...........................................................

    // ...........................................................
    public DefaultSchedulingStrategist()
    {
        assert (trueWhenFailed || falseWhenFailed || exceptionWhenFailed);
        transformationChooseMap = new LongIntTable();
        nodeSSIMap = new HashMap<NodeContext, ISchedulingStrategyInfo>();
    }

    // ~ Methods
    // ................................................................

    // ................................................................
    public String getCopyrightNotice()
    {
        return null;
    }

    public void enterSimulation()
    {
        numNonScriptedScopes++;
    }

    public void exitSimulation()
    {
        numNonScriptedScopes--;
    }

    public boolean isInSimulatingScope()
    {
        return numNonScriptedScopes > 0;
    }

    public void disableInterleaving()
    {
        interleavingSuppressed = true;
    }

    public void enableInterleaving()
    {
        interleavingSuppressed = false;
    }

    public boolean isEnabled(IState state, Transformation t, int threadId)
    {
        Exp exp = t.getOptionalExp();

        if (exp == null)
        {
            return true;
        }

        ISchedulingStrategyContext ssc = createContext(-1, -1, threadId, state);
        ArrayList<IValue> values = new ArrayList<IValue>();
        ISchedulingStrategyInfo ssi;

        do
        {
            int oldIndex = currentIndex;
            Node oldNode = currentNode;
            NodeContext oldEC = ec;
            ISchedulingStrategyInfo oldDSSI = currentSSI;

            ss.enter(ssc, exp);

            ssi = ss.newStrategyInfo();

            try
            {
                values.add(ee.evaluate(ssc, exp, ssi));
            }
            catch (BogorException e)
            {
                if (exceptionWhenFailed)
                {
                    IllFormedModelBogorException ifmmce = new IllFormedModelBogorException();
                    ifmmce.setNode(t);
                    throw ifmmce;
                }
                else if (trueWhenFailed)
                {
                    values.add(vf.newIntValue(1));
                }
                else if (falseWhenFailed)
                {
                    values.add(vf.newIntValue(0));
                }
                else
                {
                    assert false;
                }
            }
            finally
            {
                ss.exit();
                currentIndex = oldIndex;
                currentNode = oldNode;
                ec = oldEC;
                currentSSI = oldDSSI;
            }
        }
        while (!ssi.isCovered());

        int size = values.size();

        for (int i = 0; i < size; i++)
        {
            if (((IIntValue) values.get(i)).getInteger() == 1)
            {
                return true;
            }
        }

        return false;
    }

    public IntObjectTable<ArrayList<Transformation>> getEnabledTransformations(
        IEnabledTransformationsContext etc)
    {
        return getEnabledTransformations(etc, null);
    }

    public IntObjectTable<ArrayList<Transformation>> getEnabledTransformations(
        IEnabledTransformationsContext etc,
        Set<Transformation> ignoredTransformations)
    {
        assert etc != null;

        IState state = etc.getState();
        int[] threadIds = etc.getThreadIds();
        assert threadIds != null;

        IntObjectTable<ArrayList<Transformation>> result = new IntObjectTable<ArrayList<Transformation>>();
        int size = threadIds.length;

        boolean hasIgnoredTransformations = ignoredTransformations != null;

        for (int i = 0; i < size; i++)
        {
            int threadId = threadIds[i];
            int locDesc = state.getLocation(threadId);
            String locId = symbolTable.getLocDescLocIdTable()[locDesc];
            Location l = getFSMSymbolTable(state, threadId)
                .getLocationDefTable()
                .get(locId);
            int size2 = l.getTransformationCount();

            for (int j = 0; j < size2; j++)
            {
                Transformation t = l.getTransformation(j);

                if (hasIgnoredTransformations
                    && ignoredTransformations.contains(t))
                {
                    continue;
                }

                if (ss.isEnabled(state, t, threadId))
                {
                    ArrayList<Transformation> ets = result.get(threadId);

                    if (ets == null)
                    {
                        ets = new ArrayList<Transformation>();
                        result.put(threadId, ets);
                    }

                    ets.add(t);
                }
            }
        }

        // if in atomic mode, explicitly disable all threads except the
        // last one to run
        if (interleavingSuppressed)
        {
            // figure out the tid of last transition executed
            ArrayList<ITransformationBacktrackingInfo> backtrackingInfos = sr
                .getBacktrackingInfos();

            // if we could determine last thread moved, then filter out
            // all other transitions
            if (!backtrackingInfos.isEmpty())
            {
                ITransformationBacktrackingInfo lastTbi = backtrackingInfos
                    .get(backtrackingInfos.size() - 1);
                int lastMovedThread = lastTbi.getTransition().first;

                for (int tid : result.keys())
                {
                    if (tid != lastMovedThread)
                    {
                        result.remove(tid);
                    }
                }
            }
            else
            {
                // This case should only occur if Verify.beginAtomic() is the
                // very first thing called.
            }
        }

        // Now filter out transitions according to user plugins
        for (ITransformationFilter tf : getTransformationFilters())
        {
            tf.filter(result, etc);
        }

        return result;
    }

    public IMessageStore setOptions(String key, Properties configuration)
    {
        assert ((key != null) && (configuration != null));

        final String TRUE_WHEN_FAILED_ID = key + "." + this.TRUE_WHEN_FAILED_ID;
        final String FALSE_WHEN_FAILED_ID = key + "."
                                            + this.FALSE_WHEN_FAILED_ID;
        final String EXCEPTION_WHEN_FAILED_ID = key + "."
                                                + this.EXCEPTION_WHEN_FAILED_ID;
        final String TRANSFORMATION_FILTER_ID = key
                                                + "."
                                                + ISchedulingStrategist.TRANSFORMATION_FILTER_ID;

        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
        ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

        for (Iterator<Object> i = configuration.keySet().iterator(); i
            .hasNext();)
        {
            String optionId = (String) i.next();
            String value = configuration.getProperty(optionId);

            if (TRUE_WHEN_FAILED_ID.equals(optionId))
            {
                try
                {
                    trueWhenFailed = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }

                if (trueWhenFailed)
                {
                    falseWhenFailed = false;
                    exceptionWhenFailed = false;
                }
            }
            else if (FALSE_WHEN_FAILED_ID.equals(optionId))
            {
                try
                {
                    falseWhenFailed = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }

                if (falseWhenFailed)
                {
                    trueWhenFailed = false;
                    exceptionWhenFailed = false;
                }
            }
            else if (EXCEPTION_WHEN_FAILED_ID.equals(optionId))
            {
                try
                {
                    exceptionWhenFailed = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }

                if (exceptionWhenFailed)
                {
                    trueWhenFailed = false;
                    falseWhenFailed = false;
                }
            }
            else if (TRANSFORMATION_FILTER_ID.equals(optionId))
            {
                try
                {
                    List<String> list = Util.splitCommaSeparatedList(value);
                    transformationFilterClassNames = list
                        .toArray(new String[list.size()]);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId,
                                "comma-separated string list (no whitespace)",
                                "\"" + value + "\""
                            }));
                }
            }
            else if (optionId.startsWith(key) && !optionId.equals(key))
            {
                warnings.add(FileMessage.buildMessage(
                    optionId,
                    ConfigurationMessages.UNKNOWN_OPTION,
                    new String[]
                        {
                            optionId
                        }));
            }
        }

        return new DefaultMessageStore(errors, warnings);
    }

    public IntObjectTable<ArrayList<Transformation>> getWorkSet(
        IEnabledTransformationsContext etc,
        IntObjectTable<ArrayList<Transformation>> baseEnabledSet)
    {
        IntObjectTable<ArrayList<Transformation>> result = new IntObjectTable<ArrayList<Transformation>>();

        for (int key : baseEnabledSet.keys())
        {
            ArrayList<Transformation> value = baseEnabledSet.get(key);
            ArrayList<Transformation> newValue = new ArrayList<Transformation>(
                value.size());
            newValue.addAll(value);
            result.put(key, newValue);
        }

        return result;
    }

    public ITransformationFilter[] getTransformationFilters()
    {
        return transformationFilters;
    }

    public int advise(
        ISchedulingStrategyContext ssc,
        Transformation[] transformations,
        ISchedulingStrategyInfo ssi)
    {
        assert (ssc != null);
        assert (Util.assertNonNull(transformations));

        if (transformations.length == 1)
        {
            return 0;
        }

        int infoCount = ssi.getInfoCount();

        assert infoCount == 0 || infoCount == 1;

        boolean partiallyCovered = infoCount == 1;

        if (partiallyCovered)
        {
            int newChoice = ssi.getChosenIndex(0) + 1;

            ssi.setChosenIndex(0, newChoice);

            return newChoice;
        }
        else
        {
            int newChoice = 0;

            ssi.addInfo(0, transformations.length, newChoice);

            return newChoice;
        }
    }

    public int advise(
        ISchedulingStrategyContext ssc,
        List<Pair<Integer, Transformation>> choices,
        ISchedulingStrategyInfo ssi)
    {
        assert choices != null;
        assert (ssc != null);

        if (choices.size() == 1)
        {
            return 0;
        }

        long stateId = ssc.getStateId();
        long key = (stateId << 32L) + ssc.getInvisibleMoves();

        if (transformationChooseMap.containsKey(key))
        {
            assert ssi.getInfoCount() == 1;

            int lastChoose = transformationChooseMap.get(key);
            int choose = lastChoose + 1;
            transformationChooseMap.put(key, choose);
            ssi.setChosenIndex(0, choose);

            if ((choose + 1) == choices.size())
            {
                transformationChooseMap.remove(key);
            }

            return choose;
        }
        else
        {
            assert ssi.getInfoCount() == 0;

            int chosenIndex = 0;
            ssi.addInfo(0, choices.size(), chosenIndex);

            if (choices.size() != 1)
            {
                transformationChooseMap.put(key, chosenIndex);
            }

            return chosenIndex;
        }
    }

    public int advise(
        int extDesc,
        Node node,
        IValue[] choices,
        ISchedulingStrategyInfo ssi)
    {
        assert ((node != null) && (currentNode != null));
        assert (Util.assertNonNull(choices));
        assert (choices.length > 0);

        if (choices.length == 1)
        {
            return 0;
        }

        int infoCount = currentSSI.getInfoCount();

        if (currentIndex == infoCount)
        {
            int result = 0;

            // add a new record onto the current's node's stateful
            // description of which branches have been taken
            currentSSI.addInfo(extDesc, choices.length, result);

            // add this choice to the history of scheduling decisions made
            ssi.addInfo(extDesc, choices.length, result);

            currentIndex++;

            return result;
        }
        else
        {
            // sanity check: number of branches on input must equal the number
            // recorded in the stateful private scheduling record
            // ("currentDSSI")
            assert choices.length == currentSSI.getChoiceCount(currentIndex);

            int result = currentSSI.getChosenIndex(currentIndex);

            // add this choice to the history of scheduling decisions made
            ssi.addInfo(extDesc, choices.length, result);

            // "result" is an index
            assert choices.length > result;

            currentIndex++;

            return result;
        }
    }

    public IMessageStore connect(IBogorConfiguration bc)
    {
        assert (bc != null);

        symbolTable = bc.getSymbolTable();
        ss = bc.getSchedulingStrategist();
        vf = bc.getValueFactory();
        ee = bc.getExpEvaluator();
        sr = bc.getSearcher();

        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();

        ArrayList<ITransformationFilter> transFilterList = new ArrayList<ITransformationFilter>(
            transformationFilterClassNames.length);

        for (int i = 0; i < transformationFilterClassNames.length; i++)
        {
            int prevErrorCount = errors.size();

            ITransformationFilter f = (ITransformationFilter) bc
                .getModuleInstance(
                    transformationFilterClassNames[i],
                    ITransformationFilter.class,
                    errors);

            if ((f == null) || (prevErrorCount != errors.size()))
            {
                // do nothing. Errors will be passed back in return
                // value
            }
            else
            {
                f.setOptions(TRANSFORMATION_FILTER_ID, bc.getConfiguration());
                f.connect(bc);

                transFilterList.add(f);
            }
        }

        transformationFilters = transFilterList
            .toArray(new ITransformationFilter[transFilterList.size()]);

        return new DefaultMessageStore(errors, new ArrayList<FileMessage>());
    }

    public void dispose()
    {
        symbolTable = null;
        ss = null;
        vf = null;
        ee = null;
        sr = null;

        HashSet<IModule> disposedModules = new HashSet<IModule>();

        if (transformationChooseMap != null)
        {
            transformationChooseMap.clear();
            transformationChooseMap = null;
        }

        if (nodeSSIMap != null)
        {
            nodeSSIMap.clear();
            nodeSSIMap = null;
        }

        for (ITransformationFilter tf : transformationFilters)
        {
            if (!disposedModules.contains(tf))
            {
                disposedModules.add(tf);
                tf.dispose();
            }
        }

        disposedModules.clear();
        transformationFilters = EMPTY_FILTER_SET;
    }

    public void enter(ISchedulingStrategyContext ssc, Node node)
    {
        assert ((node != null) && (currentNode == null));
        currentIndex = 0;
        currentNode = node;

        int threadId = ssc.getThreadId();
        int[] locStack = (Util.search(ssc.getState().getThreadIds(), threadId) < 0)
            ? null
            : ssc.getState().getLocationStack(threadId);
        ec = new NodeContext(ssc.getStateId(), ssc.getInvisibleMoves(), ssc
            .getThreadId(), locStack, node);
        currentSSI = nodeSSIMap.get(ec);

        if (currentSSI == null)
        {
            currentSSI = ss.newStrategyInfo();
            nodeSSIMap.put(ec, currentSSI);
        }
        else
        {
            next();
        }
    }

    public void exit()
    {
        assert (currentNode != null);

        int infoCount = currentSSI.getInfoCount();

        for (int i = currentIndex; i < infoCount; i++)
        {
            int length = currentSSI.getChoiceCount(currentIndex);
            currentSSI.setChosenIndex(currentIndex, length - 1);
        }

        if (currentSSI.isCovered())
        {
            nodeSSIMap.remove(ec);
        }

        ec = null;
        currentNode = null;
        currentSSI = null;
    }

    public ISchedulingStrategyInfo newStrategyInfo()
    {
        return new DefaultSchedulerStrategyInfo();
    }

    protected FSMSymbolTable getFSMSymbolTable(IState state, int threadId)
    {
        return symbolTable.getFSMSymbolTable(state.getLocation(threadId));
    }

    protected ISchedulingStrategyContext createContext(
        final int stateId,
        final int invisibleMoves,
        final int threadId,
        final IState state)
    {
        return new ISchedulingStrategyContext()
            {
                public void dispose()
                {
                }

                public int getExtDesc()
                {
                    return 0;
                }

                public IState getState()
                {
                    return state;
                }

                public int getInvisibleMoves()
                {
                    return invisibleMoves;
                }

                public int getThreadId()
                {
                    return threadId;
                }

                public int getStateId()
                {
                    return stateId;
                }
            };
    }

    /**
     * Set up the bookkeeping so that each choice point for the current action
     * will point to the next option (compared to last time).
     */
    protected void next()
    {
        int infoCount = currentSSI.getInfoCount();

        // iterate from innermost (rightmost) to outermost (leftmost)
        // expression needing advanced

        boolean allToRhsWrapped = true;

        for (int i = infoCount - 1; i >= 0; i--)
        {
            if (!allToRhsWrapped)
            {
                break;
            }

            int numChoices = currentSSI.getChoiceCount(i);
            int lastChoice = currentSSI.getChosenIndex(i);

            int newChoice = (lastChoice + 1) % numChoices;

            if (newChoice != 0)
            {
                // all choices earlier (to the left) will not advance,
                // since this option has not fully exhausted yet
                allToRhsWrapped = false;
            }

            currentSSI.setChosenIndex(i, newChoice);
        }
    }

    // ~ Classes
    // ................................................................

    // ................................................................
    protected final class DefaultSchedulerStrategyInfo
        implements ISchedulingStrategyInfo
    {
        private IntList list;

        public DefaultSchedulerStrategyInfo()
        {
            this(new IntList(3));
        }

        public void addInfo(int extId, int choiceCount, int chosenIndex)
        {
            this.list.add(extId);
            this.list.add(choiceCount);
            this.list.add(chosenIndex);
        }

        public DefaultSchedulerStrategyInfo(IntList list)
        {
            this.list = list;
        }

        public int getExtId(int infoIndex)
        {
            return list.get(infoIndex * 3);
        }

        public int getChoiceCount(int infoIndex)
        {
            return list.get((infoIndex * 3) + 1);
        }

        public int getChosenIndex(int infoIndex)
        {
            return list.get((infoIndex * 3) + 2);
        }

        public void setChosenIndex(int infoIndex, int newChosenValue)
        {
            list.set((infoIndex * 3) + 2, newChosenValue);
        }

        public boolean isCovered()
        {
            int size = list.size();

            for (int i = 0; i < size; i += 3)
            {
                /*
                 * Position (i + 1) tells how many total options were available
                 * Position (i + 2) tells how many many options have been taken
                 * so far, minus 1
                 */
                if (list.get(i + 1) != (list.get(i + 2) + 1))
                {
                    return false;
                }
            }

            return true;
        }

        public int getInfoCount()
        {
            return list.size() / 3;
        }

        public ISchedulingStrategyInfo clone(Map<Object, Object> cloneMap)
        {
            DefaultSchedulerStrategyInfo dssi = (DefaultSchedulerStrategyInfo) cloneMap
                .get(this);

            if (dssi != null)
            {
                return dssi;
            }

            dssi = new DefaultSchedulerStrategyInfo();
            cloneMap.put(this, dssi);

            dssi.list.add(list.toArray());

            return dssi;
        }

        public boolean hasInfo()
        {
            return list.size() != 0;
        }

        public String toString()
        {
            StringBuffer sb = new StringBuffer();
            int size = list.size();

            for (int i = 0; i < size; i++)
            {
                sb.append(list.get(i));

                if (i != (size - 1))
                {
                    sb.append(" ");
                }
            }

            return sb.toString();
        }
    }

    protected final class NodeContext
    {
        // ~ Instance variables
        // .................................................

        // .................................................
        Node node;

        int stateId;

        int invisibleMoves;

        int[] locStack;

        int threadId;

        // ~ Constructors
        // .......................................................

        // .......................................................
        NodeContext(
            int stateId,
            int invisibleMoves,
            int threadId,
            int[] locStack,
            Node node)
        {
            this.stateId = stateId;
            this.invisibleMoves = invisibleMoves;
            this.threadId = threadId;
            this.locStack = locStack;
            this.node = node;
        }

        // ~ Methods
        // ............................................................

        // ............................................................
        public boolean equals(Object o)
        {
            NodeContext other = (NodeContext) o;

            boolean flag = (stateId == other.stateId)
                           && (invisibleMoves == other.invisibleMoves)
                           && (threadId == other.threadId)
                           && (node == other.node);

            if (flag)
            {
                if ((locStack == null) && (other.locStack == null))
                {
                    return true;
                }
                else if ((locStack == null) || (other.locStack == null))
                {
                    return false;
                }

                for (int i = 0; i < locStack.length; i++)
                {
                    if (locStack[i] != other.locStack[i])
                    {
                        return false;
                    }
                }

                return true;
            }
            else
            {
                return false;
            }
        }

        public int hashCode()
        {
            int result = (locStack == null) ? 0 : (locStack.length << 4);
            result += ((stateId + invisibleMoves) << (1 + threadId) << (2 + node
                .hashCode()) << 3);

            return result;
        }
    }

    /**
     * @return a set of tuples whose first element says the name of the option,
     *         and whose second element says whether the option is required, and
     *         whose third element says whether the option is private to this
     *         module (and thus prefixed by the interface implemented, e.g.,
     *         <code>edu.ksu.cis.projects.bogor.module.ISearcher</code>) or
     *         global in scope (and thus no qualifier is prepended).
     */
    public Collection<Triple<String, Boolean, OptionScope>> getOptionIds()
    {
        ArrayList<Triple<String, Boolean, OptionScope>> result;
        result = new ArrayList<Triple<String, Boolean, OptionScope>>();

        for (String id : new String[]
            {
                TRUE_WHEN_FAILED_ID, FALSE_WHEN_FAILED_ID,
                EXCEPTION_WHEN_FAILED_ID, TRANSFORMATION_FILTER_ID
            })
        {
            result.add(new Triple<String, Boolean, OptionScope>(
                id,
                Boolean.FALSE,
                OptionScope.MODULE));
        }

        return result;
    }

    /**
     * @return a tuple whose first element says the domain of the option values,
     *         and whose second element says whether the option is multivalued
     *         (that is, a comma-separated list)
     */
    public Pair<Domain, Boolean> getOptionDomain(String id)
    {
        for (String boolId : new String[]
            {
                TRUE_WHEN_FAILED_ID, FALSE_WHEN_FAILED_ID,
                EXCEPTION_WHEN_FAILED_ID
            })
        {
            if (boolId.equals(id))
            {
                return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
            }
        }

        if (TRANSFORMATION_FILTER_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.STRING, Boolean.TRUE);
        }

        return null;
    }

    public Collection<String> getSuggestedValues(
        String id,
        IBogorConfiguration bc,
        SymbolTable st)
    {
        ArrayList<String> result = new ArrayList<String>();

        for (String boolId : new String[]
            {
                TRUE_WHEN_FAILED_ID, FALSE_WHEN_FAILED_ID,
                EXCEPTION_WHEN_FAILED_ID
            })
        {
            if (boolId.equals(id))
            {
                result.add("true");
                result.add("false");
            }
        }

        if (ISchedulingStrategist.TRANSFORMATION_FILTER_ID.equals(id))
        {
            for (Class c : bc
                .getKnownImplementingClasses(ITransformationFilter.class))
            {
                result.add(c.getCanonicalName());
            }
        }

        return result;
    }

    /**
     * Checks whether the value of a configuration option is legal.
     * 
     * @param id
     *            the option's name, as returned by the first tuple element of
     *            an item returned by {@link #getOptionIds()}
     * @param value
     *            the value of the option, or <code>null</code> if unconfigued
     * @param st
     *            the symbol table for the BIR model
     * @param errors
     *            a container into which errors should be put. Implementors
     *            should not assume that <code>errors</code> is empty upon
     *            entry into this method; it may aggregate the results of
     *            calling <code>validate</code> on many
     *            <code>ISelfDescribingModule</code> instances.
     * @return <code>true</code> iff the option is supported and its value is
     *         legal
     */
    public boolean validate(
        String id,
        String value,
        IBogorConfiguration bc,
        SymbolTable st,
        Collection<FileMessage> errors)
    {
        Pair<Domain, Boolean> domain = getOptionDomain(id);

        // If the option is unknown, then call it a bad value
        if (domain == null)
        {
            return false;
        }

        // No option in this module is required, so a blank value
        // will be considered OK
        if (value == null)
        {
            return true;
        }

        switch (domain.first)
        {
            case BOOLEAN:
                if (!"true".equalsIgnoreCase(value)
                    && !"false".equalsIgnoreCase(value))
                {
                    errors.add(FileMessage.buildMessage(
                        "Expecting boolean",
                        new String[0]));
                    return false;
                }
                break;

            case STRING:
                if (TRANSFORMATION_FILTER_ID.equals(id))
                {
                    int prevErrorCount = errors.size();

                    for (String className : Util.splitCommaSeparatedList(value))
                    {
                        // adds one or more messages to the errors collection if
                        // the requested class can't be found
                        bc.getModuleInstance(
                            className,
                            ITransformationFilter.class,
                            errors);
                    }

                    if (prevErrorCount != errors.size())
                    {
                        // couldn't instantiate at least one of the options
                        return false;
                    }
                }
                break;

            default:
                break;
        }

        return true;
    }
}
